src/Pure/Isar/proof_context.ML
changeset 77979 a12c48fbf10f
parent 77970 31ea5c1f874d
child 78050 f16067da45ef
equal deleted inserted replaced
77978:14d133cff073 77979:a12c48fbf10f
  1074   |> Context_Position.restore_visible ctxt
  1074   |> Context_Position.restore_visible ctxt
  1075   |> restore_naming ctxt;
  1075   |> restore_naming ctxt;
  1076 
  1076 
  1077 end;
  1077 end;
  1078 
  1078 
  1079 fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) false b c) ctxt;
  1079 fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
  1080 
  1080 
  1081 
  1081 
  1082 
  1082 
  1083 (** basic logical entities **)
  1083 (** basic logical entities **)
  1084 
  1084