Code improvement: use actual proof context.
adbrucker/isabelle-hacks/master This commit looks good
Details
adbrucker/isabelle-hacks/master This commit looks good
Details
This commit is contained in:
parent
446792928e
commit
dd8a141d5d
|
@ -702,7 +702,6 @@ structure Nano_Json_Serialize_Isar = struct
|
||||||
let
|
let
|
||||||
val thy = Proof_Context.theory_of ctxt
|
val thy = Proof_Context.theory_of ctxt
|
||||||
val master_dir = Resources.master_directory thy
|
val master_dir = Resources.master_directory thy
|
||||||
val ctxt = Proof_Context.init_global thy;
|
|
||||||
val term = Thm.concl_of (Global_Theory.get_thm thy (json_const^"_def"))
|
val term = Thm.concl_of (Global_Theory.get_thm thy (json_const^"_def"))
|
||||||
val json_term = case term of
|
val json_term = case term of
|
||||||
_ $ (_ $ json_term) => json_term
|
_ $ (_ $ json_term) => json_term
|
||||||
|
|
Loading…
Reference in New Issue